Proof development primitives #1637

robdockins · 2022-04-22T17:25:25Z

This PR reorganizes the execution internals of SAWScript and implements some additional experimental primitives that will hopefully yield quality-of-life improvements for proof development.

The two main new capabilities are a callcc primitive, and a subshell primitive. The subshell primitive, when executed, will drop the user directly into a REPL session with the same context as the point where subshell was called. This should allow the user to experiment, view internal state, etc. interactively. callcc, as typical, reifies the rest of the computation as a function that can be called. This is especially useful in combination with subshell, as the user can experiment with state updates and see what effect that has on the remainder of the proof without having to rerun the proof from the beginning.

There is additionally a new checkpoint primitive that captures (some) of the mutable state of the system and allows it to be restored at a later time. This facility is highly experimental, and it is relatively easy to work yourself into broken states using it. Probably, we need a more comprehensive plan to deal with the general idea of checkpoint/resume in the entire SAW ecosystem to make this work more reliably.

robdockins · 2022-04-22T17:32:49Z

Here is a quick example of what this makes possible. Consider the following SAW script, and the following interaction.

enable_experimental;

let interactive =
  callcc (\ (done : Int -> TopLevel ()) ->
      rec retry (u: ()) : TopLevel Int =
        do{ reset <- checkpoint;
	    print "<<Interactive subshell>>";
            subshell ();
	    reset ();
	    retry (); }
      in retry ());

x <- interactive;

print (str_concat "x = " (show x));
print (str_concat "y = " (show y));

$ saw interactive.saw


[17:28:17.889] Loading file "/Users/rdockins/code/saw-script/interactive.saw"
[17:28:17.890] <<Interactive subshell>>
sawscript> let y = 10
sawscript> done 42
[17:28:28.472] x = 42
[17:28:28.472] y = 10
sawscript> let y = 12
sawscript> done 100
[17:28:37.856] x = 100
[17:28:37.856] y = 12
sawscript> ^D
[17:28:39.064] Restoring state from checkpoint
[17:28:39.064] <<Interactive subshell>>
sawscript> done 100
[17:28:41.496] x = 100

/Users/rdockins/code/saw-script/interactive.saw:16:27-16:33: Unbound variable: "y" (/Users/rdockins/code/saw-script/interactive.saw:16:32-16:33)
Note that some built-in commands are available only after running
either `enable_deprecated` or `enable_experimental`.

sawscript> exit 0

chameco · 2022-04-24T22:15:44Z

This is really neat! Some thoughts before looking at the code:

I've been thinking a lot recently about to-disk serialization for Terms, and maybe even of the SAW context at large. It seems like at least some of the work to make checkpoint or continuations less broken would also make this serialization more doable - things like making sure important state lives somewhere accessible instead of hidden inside a closure somewhere, and solving problems related to moving Terms between SharedContexts.

We should also think about the Python story. I think a debugging tool like subshell will be very useful, but it will further widen the (already substantial in my opinion) user experience gap between SAWScript and the Python interface.

chameco · 2022-04-24T22:24:02Z

src/SAWScript/Builtins.hs

-  Prover.writeSAIGInferLatches path1 t1
-  Prover.writeSAIGInferLatches path2 t2
-  io $ callCommand (abcDsec path1 path2)
+  write_t1 <- Prover.writeSAIGInferLatches t1


I think these AIG-related changes might be unrelated work that was caught in the first commit.

This is actually related, although the reason is pretty subtle. TopLevel no longer has a MonadMask instance, as continuation-based monads don't provide the necessary guarantees. However withSystemTempFile demands MonadMask in order to manage the temporary file lifetime. So, one solution is this, where we extract an IO action from the TopLevel and execute it later in an IO context.

This seems to be the only place that MonadMask instance was being used.

Ah, makes sense. Thanks for the clarification.

intTests/test_external_abc/test.saw

chameco · 2022-04-24T22:26:54Z

src/SAWScript/Interpreter.hs

+  , prim "subshell"            "() -> TopLevel ()"
+    (\_ _ -> toplevelSubshell)
+    Experimental
+    []


We should make sure to include documentation for subshell before merging.

chameco · 2022-04-24T22:27:32Z

src/SAWScript/Prover/Exporter.hs

@@ -203,13 +203,16 @@ writeSAIG file tt numLatches = do

 -- | Given a term a type '(i, s) -> (o, s)', call @writeSAIG@ on term
 -- with latch bits set to '|s|', the width of 's'.
-writeSAIGInferLatches :: FilePath -> TypedTerm -> TopLevel ()
-writeSAIGInferLatches file tt = do
+writeSAIGInferLatches :: TypedTerm -> TopLevel (FilePath -> IO ())


Maybe an unrelated change?

robdockins · 2022-04-25T15:31:56Z

This is really neat! Some thoughts before looking at the code:

I've been thinking a lot recently about to-disk serialization for Terms, and maybe even of the SAW context at large. It seems like at least some of the work to make checkpoint or continuations less broken would also make this serialization more doable - things like making sure important state lives somewhere accessible instead of hidden inside a closure somewhere, and solving problems related to moving Terms between SharedContexts.

Agreed, these are all important and useful problems to be addressing, and should help with this kind of brokeness.

We should also think about the Python story. I think a debugging tool like subshell will be very useful, but it will further widen the (already substantial in my opinion) user experience gap between SAWScript and the Python interface.

Also agreed. In some ways, I feel like the Python story is already ahead here, but the user-facing interaction needs some work.

robdockins · 2022-04-25T15:37:37Z

Is this what it looks like when we hit the CI memory limits?

[20:55:12.365] Branching on 1 override variants of OPENSSL_malloc ...
[20:55:12.365] Applied override! OPENSSL_malloc
[20:55:12.366] Symbolic simulation completed with side conditions.
[20:55:12.399] Checking proof obligations ECDSA_do_sign ...
Killed
137
make: *** [awslc] Error 137
Makefile:25: recipe for target 'awslc' failed

RyanGlScott · 2022-04-25T15:44:13Z

Is this what it looks like when we hit the CI memory limits?

Most likely. I've seen the same error code (137) in the CI for #1563 as well.

robdockins · 2022-04-25T16:45:46Z

According to my local readings, the memory usage of this branch is only very slightly higher than for master, but I guess we are right on that knife edge.

RyanGlScott · 2022-06-27T12:44:56Z

FYI, the CI on this is not running due to a merge conflict (most likely with #1695).

robdockins · 2022-07-07T17:04:47Z

Seems like this is now squeaking under the memory limits.... I'll work on getting this a little more polished up and see if we can get it merged.

chameco

LGTM, although it looks like there's some weirdness happening with the macOS CI. I can grab and unzip the supposedly problematic zip file, so maybe just an Actions hiccup?

robdockins · 2022-07-25T20:16:06Z

Logs indicate some kind of failure downloading what4-solvers...

robdockins · 2022-07-26T15:17:24Z

Whelp... looks like we're failing on memory limits again.

StateContT transformer, which gives us the ability to capture continuations. This allows us to implement `callcc` as a saw-script command. Additionally, implement a "checkpoint" command that will capture the TopLevel monad state and allow it to be restored later. Also, rework some aspects of error handling. The previous method no longer worked properly with a continuation-based TopLevel monad.

When invoked from a batch file (or from an ongoing REPL session) starts a "subshell" REPL session. The intent here is to allow for exploration and experimentation in the middle of a larger run. For now, subshells are not very useful, as there isn't a good way to expose the local SAW environment to the shell.

of the TopLevel monad. This allows it to interact with primitive operations; in particular, we can start a subshell with local SAW script bindings in scope.

be leaving alone (async and exit exceptions).

`NameSeeds` value used internally by Cryptol to be carried forward across checkpoints. This prevents internal nonce values from being reused, which, in turn, avoids errors about registering duplicate names. It is unclear if this is the correct long-term fix, but it allows checkpoint to work more reliably when importing Cryptol modules or using `let {{ ... }}` constructs.

mutable state part of the TopLevel monad. This allows them to participate in the checkpoint/restore mechanism.

``` void saw_assert( uint32_t ); ``` This allows the program source to directly assert a proposition inline which is then assumed as part of the path condition. This can sometimes help the path sat checker by stating helpful lemmas whose proof can be deferred to the VC-checking phase. It can also be helpful for program/proof exploration, allowing the user to directly state inline hypotheses about program behavior, and then attempt to prove them.

allows the user to restore proof states.

robdockins · 2022-08-08T19:47:16Z

After a rebase, this is back under memory limits... I think I'm going to go ahead and merge it, even though the CI seems a bit erratic.

robdockins requested review from brianhuffman and chameco April 22, 2022 17:25

robdockins force-pushed the rwd/dev-tools branch from 8c25b3d to 9ed30cd Compare April 22, 2022 19:51

chameco reviewed Apr 24, 2022

View reviewed changes

chameco mentioned this pull request Apr 24, 2022

Improve the UX of the Python API #1639

Open

robdockins force-pushed the rwd/dev-tools branch from 03045b8 to ac2a910 Compare April 27, 2022 23:37

robdockins force-pushed the rwd/dev-tools branch from 499112e to 29ea30a Compare May 20, 2022 22:27

robdockins marked this pull request as draft June 1, 2022 17:46

robdockins force-pushed the rwd/dev-tools branch 2 times, most recently from 89b408c to 7f8f5ef Compare June 7, 2022 16:36

robdockins force-pushed the rwd/dev-tools branch from 7f8f5ef to f15b8cd Compare June 23, 2022 23:33

robdockins force-pushed the rwd/dev-tools branch 2 times, most recently from 8c74519 to 1084357 Compare July 6, 2022 16:57

robdockins force-pushed the rwd/dev-tools branch 2 times, most recently from 0907c55 to 9c451cb Compare July 25, 2022 19:52

robdockins marked this pull request as ready for review July 25, 2022 19:52

robdockins requested review from chameco and removed request for brianhuffman July 25, 2022 19:52

chameco approved these changes Jul 25, 2022

View reviewed changes

robdockins added 13 commits August 8, 2022 09:38

Push the SAW script "local environment" into the read-only section

7a305d7

of the TopLevel monad. This allows it to interact with primitive operations; in particular, we can start a subshell with local SAW script bindings in scope.

Prevent the REPL from grabbing and printing exceptions it should

dbe32ba

be leaving alone (async and exit exceptions).

Fix the saw-remote-api build

d9f6ba0

Move the SharedContext and TheoremDB objects into the

8bb8cae

mutable state part of the TopLevel monad. This allows them to participate in the checkpoint/restore mechanism.

Add checkpoint capabilities to the SharedContext

8780ee2

Add checkpoint/resume commands to REPL command invocations.

d942988

Add a proof script version of subshell

4101e38

Update saw-remote-api

eef3bb4

Add help strings to the subshell and proof_subshell commands.

b8d17bc

Add a proof_checkpoint command that captures and

6952456

allows the user to restore proof states.

robdockins force-pushed the rwd/dev-tools branch from 9c451cb to 6952456 Compare August 8, 2022 16:39

robdockins merged commit 6cbe62a into master Aug 8, 2022

mergify bot deleted the rwd/dev-tools branch August 8, 2022 19:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Proof development primitives #1637

Proof development primitives #1637

robdockins commented Apr 22, 2022

robdockins commented Apr 22, 2022

chameco commented Apr 24, 2022

chameco Apr 24, 2022

robdockins Apr 25, 2022

chameco Apr 25, 2022

chameco Apr 24, 2022

chameco Apr 24, 2022

robdockins commented Apr 25, 2022

robdockins commented Apr 25, 2022

RyanGlScott commented Apr 25, 2022

robdockins commented Apr 25, 2022

RyanGlScott commented Jun 27, 2022

robdockins commented Jul 7, 2022

chameco left a comment

robdockins commented Jul 25, 2022

robdockins commented Jul 26, 2022

robdockins commented Aug 8, 2022

Proof development primitives #1637

Proof development primitives #1637

Conversation

robdockins commented Apr 22, 2022

robdockins commented Apr 22, 2022

chameco commented Apr 24, 2022

chameco Apr 24, 2022

Choose a reason for hiding this comment

robdockins Apr 25, 2022

Choose a reason for hiding this comment

chameco Apr 25, 2022

Choose a reason for hiding this comment

chameco Apr 24, 2022

Choose a reason for hiding this comment

chameco Apr 24, 2022

Choose a reason for hiding this comment

robdockins commented Apr 25, 2022

robdockins commented Apr 25, 2022

RyanGlScott commented Apr 25, 2022

robdockins commented Apr 25, 2022

RyanGlScott commented Jun 27, 2022

robdockins commented Jul 7, 2022

chameco left a comment

Choose a reason for hiding this comment

robdockins commented Jul 25, 2022

robdockins commented Jul 26, 2022

robdockins commented Aug 8, 2022